def add (x y : Nat) := x + y